Nuprl Definition : predicate_implies
11,40
postcript
pdf
P1
P2
==
x
:
T
. (
P1
(
x
))
(
P2
(
x
))
latex
clarification:
predicate_implies(
T
;
P1
;
P2
) ==
x
:
T
. (
P1
(
x
))
(
P2
(
x
))
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
f
(
a
)
FDL editor aliases
predicate_implies
origin
P2 == 
x:T. (P1(x)) (P2(x))
x:T. (P1(x)) (P2(x)) P2 == x:T. (P1(x)) (P2(x))
x:T. (P1(x)) (P2(x)) x:A. B(x) Q